p, q:(IdLnk List), i, j, k:Id.
lconnects(p;i;j)  lconnects(q;j;k)  (r:IdLnk List. lconnects(r;i;k)) 

latex

Definitions	t  T, x:A. B(x), True, T, x:A. B(x), P  Q, , hd(l), Y, ||as||, P & Q, lconnects(p;i;j), P  Q, if b then t else f fi , ff, null(as), b, P  Q, A, False, lpath(p), tt, i <z j, b, i z j, nth_tl(n;as), l[i], last(L), A  B, i  j < k, {i..j}, P  Q, Dec(P)
Lemmas	IdLnk wf, Id wf, true wf, squash wf, lconnects wf, non neg length, length wf1, ldst wf, lpath cons, not wf, false wf, last cons, int seg wf, lnk-inv wf, decidable equal IdLnk, length cons